Nuprl Definition : inv_funs
13,42
postcript
pdf
InvFuns(
A
;
B
;
f
;
g
) == (
g
o
f
) = Id{
A
} & (
f
o
g
) = Id{
B
}
latex
clarification:
InvFuns(
A
;
B
;
f
;
g
) == (
g
o
f
) = Id{
A
}
A
A
& (
f
o
g
) = Id{
B
}
B
B
latex
Up
fun
1
,
fun
1
Wellformedness Lemmas
inv
funs
wf
,
inv
funs
wf
Definitions
P
&
Q
,
s
=
t
,
x
:
A
B
(
x
)
,
f
o
g
,
Id{
T
}
FDL editor aliases
inv_funs
origin
A
A & (f o g) = Id{B} BB AA & (f o g) = Id{B} BB B(x)